Nuprl Lemma : tagged-messages_wf 0,22
S, V:Type, M:(IdLnkIdType), l:IdLnk, s:S, v:V, L:(t:Id(SV(M(l,t) List))) List.
tagged-messages(l;s;v;L)  {m:Msg(M)| mlnk(m) = l } List 
latex

Definitions1of(t), tagged-messages(l;s;v;L), map(f;as), mlnk(m), tagged-list-messages(s;v;L), x. t(x), x:A. B(x), Msg(M), x(s1,s2), Id, IdLnk, t  T
Lemmastagged-list-messages wf, mlnk wf, map wf, Id wf, IdLnk wf, pi1 wf

origin